\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), $e$:es{-}E(${\it es}$).
\\[0ex]fischer\=\{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\Rightarrow$ (f{-}newround\{x:ut2, free:ut2, mine:ut2\}(${\it es}$; $L$; $e$) $\in$ prop\{i:l\})
\end{tabbing}